0 CpxTRS
↳1 TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID), 1 ms)
↳2 CpxWeightedTrs
↳3 TypeInferenceProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CpxTypedWeightedTrs
↳5 CompletionProof (UPPER BOUND(ID), 0 ms)
↳6 CpxTypedWeightedCompleteTrs
↳7 CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID), 0 ms)
↳8 CpxRNTS
↳9 CompleteCoflocoProof (⇔, 344 ms)
↳10 BOUNDS(1, n^2)
sort#2(Nil) → Nil
sort#2(Cons(x4, x2)) → insert#3(x4, sort#2(x2))
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1))
cond_insert_ord_x_ys_1(False, x3, x2, x1) → Cons(x2, insert#3(x3, x1))
insert#3(x2, Nil) → Cons(x2, Nil)
insert#3(x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2)
leq#2(0, x8) → True
leq#2(S(x12), 0) → False
leq#2(S(x4), S(x2)) → leq#2(x4, x2)
main(x1) → sort#2(x1)
sort#2(Nil) → Nil [1]
sort#2(Cons(x4, x2)) → insert#3(x4, sort#2(x2)) [1]
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1)) [1]
cond_insert_ord_x_ys_1(False, x3, x2, x1) → Cons(x2, insert#3(x3, x1)) [1]
insert#3(x2, Nil) → Cons(x2, Nil) [1]
insert#3(x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2) [1]
leq#2(0, x8) → True [1]
leq#2(S(x12), 0) → False [1]
leq#2(S(x4), S(x2)) → leq#2(x4, x2) [1]
main(x1) → sort#2(x1) [1]
sort#2(Nil) → Nil [1]
sort#2(Cons(x4, x2)) → insert#3(x4, sort#2(x2)) [1]
cond_insert_ord_x_ys_1(True, x3, x2, x1) → Cons(x3, Cons(x2, x1)) [1]
cond_insert_ord_x_ys_1(False, x3, x2, x1) → Cons(x2, insert#3(x3, x1)) [1]
insert#3(x2, Nil) → Cons(x2, Nil) [1]
insert#3(x6, Cons(x4, x2)) → cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2) [1]
leq#2(0, x8) → True [1]
leq#2(S(x12), 0) → False [1]
leq#2(S(x4), S(x2)) → leq#2(x4, x2) [1]
main(x1) → sort#2(x1) [1]
| sort#2 :: Nil:Cons → Nil:Cons Nil :: Nil:Cons Cons :: 0:S → Nil:Cons → Nil:Cons insert#3 :: 0:S → Nil:Cons → Nil:Cons cond_insert_ord_x_ys_1 :: True:False → 0:S → 0:S → Nil:Cons → Nil:Cons True :: True:False False :: True:False leq#2 :: 0:S → 0:S → True:False 0 :: 0:S S :: 0:S → 0:S main :: Nil:Cons → Nil:Cons |
| Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules:
The TRS has the following type information:
Rewrite Strategy: INNERMOST |
Nil => 0
True => 1
False => 0
0 => 0
cond_insert_ord_x_ys_1(z, z', z'', z1) -{ 1 }→ 1 + x2 + insert#3(x3, x1) :|: x1 >= 0, z' = x3, z1 = x1, z = 0, z'' = x2, x3 >= 0, x2 >= 0
cond_insert_ord_x_ys_1(z, z', z'', z1) -{ 1 }→ 1 + x3 + (1 + x2 + x1) :|: x1 >= 0, z = 1, z' = x3, z1 = x1, z'' = x2, x3 >= 0, x2 >= 0
insert#3(z, z') -{ 1 }→ cond_insert_ord_x_ys_1(leq#2(x6, x4), x6, x4, x2) :|: x4 >= 0, z' = 1 + x4 + x2, x6 >= 0, z = x6, x2 >= 0
insert#3(z, z') -{ 1 }→ 1 + x2 + 0 :|: z = x2, x2 >= 0, z' = 0
leq#2(z, z') -{ 1 }→ leq#2(x4, x2) :|: x4 >= 0, z' = 1 + x2, z = 1 + x4, x2 >= 0
leq#2(z, z') -{ 1 }→ 1 :|: x8 >= 0, z = 0, z' = x8
leq#2(z, z') -{ 1 }→ 0 :|: z = 1 + x12, x12 >= 0, z' = 0
main(z) -{ 1 }→ sort#2(x1) :|: x1 >= 0, z = x1
sort#2(z) -{ 1 }→ insert#3(x4, sort#2(x2)) :|: x4 >= 0, z = 1 + x4 + x2, x2 >= 0
sort#2(z) -{ 1 }→ 0 :|: z = 0
| eq(start(V, V3, V4, V5),0,[fun(V, Out)],[V >= 0]). eq(start(V, V3, V4, V5),0,[fun2(V, V3, V4, V5, Out)],[V >= 0,V3 >= 0,V4 >= 0,V5 >= 0]). eq(start(V, V3, V4, V5),0,[fun1(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4, V5),0,[fun3(V, V3, Out)],[V >= 0,V3 >= 0]). eq(start(V, V3, V4, V5),0,[main(V, Out)],[V >= 0]). eq(fun(V, Out),1,[],[Out = 0,V = 0]). eq(fun(V, Out),1,[fun(V2, Ret1),fun1(V1, Ret1, Ret)],[Out = Ret,V1 >= 0,V = 1 + V1 + V2,V2 >= 0]). eq(fun2(V, V3, V4, V5, Out),1,[],[Out = 2 + V6 + V7 + V8,V8 >= 0,V = 1,V3 = V6,V5 = V8,V4 = V7,V6 >= 0,V7 >= 0]). eq(fun2(V, V3, V4, V5, Out),1,[fun1(V10, V11, Ret11)],[Out = 1 + Ret11 + V9,V11 >= 0,V3 = V10,V5 = V11,V = 0,V4 = V9,V10 >= 0,V9 >= 0]). eq(fun1(V, V3, Out),1,[],[Out = 1 + V12,V = V12,V12 >= 0,V3 = 0]). eq(fun1(V, V3, Out),1,[fun3(V13, V14, Ret0),fun2(Ret0, V13, V14, V15, Ret2)],[Out = Ret2,V14 >= 0,V3 = 1 + V14 + V15,V13 >= 0,V = V13,V15 >= 0]). eq(fun3(V, V3, Out),1,[],[Out = 1,V16 >= 0,V = 0,V3 = V16]). eq(fun3(V, V3, Out),1,[],[Out = 0,V = 1 + V17,V17 >= 0,V3 = 0]). eq(fun3(V, V3, Out),1,[fun3(V18, V19, Ret3)],[Out = Ret3,V18 >= 0,V3 = 1 + V19,V = 1 + V18,V19 >= 0]). eq(main(V, Out),1,[fun(V20, Ret4)],[Out = Ret4,V20 >= 0,V = V20]). input_output_vars(fun(V,Out),[V],[Out]). input_output_vars(fun2(V,V3,V4,V5,Out),[V,V3,V4,V5],[Out]). input_output_vars(fun1(V,V3,Out),[V,V3],[Out]). input_output_vars(fun3(V,V3,Out),[V,V3],[Out]). input_output_vars(main(V,Out),[V],[Out]). |
CoFloCo proof output:
Preprocessing Cost Relations
=====================================
#### Computed strongly connected components
0. recursive : [fun3/3]
1. recursive : [fun1/3,fun2/5]
2. recursive [non_tail] : [fun/2]
3. non_recursive : [main/2]
4. non_recursive : [start/4]
#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into fun3/3
1. SCC is partially evaluated into fun1/3
2. SCC is partially evaluated into fun/2
3. SCC is completely evaluated into other SCCs
4. SCC is partially evaluated into start/4
Control-Flow Refinement of Cost Relations
=====================================
### Specialization of cost equations fun3/3
* CE 15 is refined into CE [16]
* CE 14 is refined into CE [17]
* CE 13 is refined into CE [18]
### Cost equations --> "Loop" of fun3/3
* CEs [17] --> Loop 11
* CEs [18] --> Loop 12
* CEs [16] --> Loop 13
### Ranking functions of CR fun3(V,V3,Out)
* RF of phase [13]: [V,V3]
#### Partial ranking functions of CR fun3(V,V3,Out)
* Partial RF of phase [13]:
- RF of loop [13:1]:
V
V3
### Specialization of cost equations fun1/3
* CE 9 is refined into CE [19,20]
* CE 10 is refined into CE [21]
* CE 8 is refined into CE [22,23]
### Cost equations --> "Loop" of fun1/3
* CEs [23] --> Loop 14
* CEs [22] --> Loop 15
* CEs [20] --> Loop 16
* CEs [21] --> Loop 17
* CEs [19] --> Loop 18
### Ranking functions of CR fun1(V,V3,Out)
* RF of phase [14,15]: [V3]
#### Partial ranking functions of CR fun1(V,V3,Out)
* Partial RF of phase [14,15]:
- RF of loop [14:1]:
V3-1
- RF of loop [15:1]:
V3
### Specialization of cost equations fun/2
* CE 12 is refined into CE [24,25,26]
* CE 11 is refined into CE [27]
### Cost equations --> "Loop" of fun/2
* CEs [27] --> Loop 19
* CEs [26] --> Loop 20
* CEs [24] --> Loop 21
* CEs [25] --> Loop 22
### Ranking functions of CR fun(V,Out)
* RF of phase [20,21]: [V]
#### Partial ranking functions of CR fun(V,Out)
* Partial RF of phase [20,21]:
- RF of loop [20:1]:
V-1
- RF of loop [21:1]:
V
### Specialization of cost equations start/4
* CE 3 is refined into CE [28]
* CE 2 is refined into CE [29,30,31]
* CE 4 is refined into CE [32,33]
* CE 5 is refined into CE [34,35,36]
* CE 6 is refined into CE [37,38,39,40]
* CE 7 is refined into CE [41,42]
### Cost equations --> "Loop" of start/4
* CEs [35,38] --> Loop 23
* CEs [28,33,36,39,40,42] --> Loop 24
* CEs [29,30,31,32,34,37,41] --> Loop 25
### Ranking functions of CR start(V,V3,V4,V5)
#### Partial ranking functions of CR start(V,V3,V4,V5)
Computing Bounds
=====================================
#### Cost of chains of fun3(V,V3,Out):
* Chain [[13],12]: 1*it(13)+1
Such that:it(13) =< V
with precondition: [Out=1,V>=1,V3>=V]
* Chain [[13],11]: 1*it(13)+1
Such that:it(13) =< V3
with precondition: [Out=0,V3>=1,V>=V3+1]
* Chain [12]: 1
with precondition: [V=0,Out=1,V3>=0]
* Chain [11]: 1
with precondition: [V3=0,Out=0,V>=1]
#### Cost of chains of fun1(V,V3,Out):
* Chain [[14,15],17]: 7*it(14)+1
Such that:aux(3) =< -V+Out
it(14) =< aux(3)
with precondition: [V+V3+1=Out,V>=1,V3>=1]
* Chain [[14,15],16]: 7*it(14)+1*s(4)+3
Such that:aux(2) =< -2*V+Out
aux(1) =< -V+Out
s(4) =< V
it(14) =< aux(1)
it(14) =< aux(2)
with precondition: [V+V3+1=Out,V>=1,V3>=V+2]
* Chain [18]: 3
with precondition: [V=0,V3+1=Out,V3>=1]
* Chain [17]: 1
with precondition: [V3=0,V+1=Out,V>=0]
* Chain [16]: 1*s(4)+3
Such that:s(4) =< V
with precondition: [V+V3+1=Out,V>=1,V3>=V+1]
#### Cost of chains of fun(V,Out):
* Chain [[20,21],22,19]: 10*it(20)+7*s(25)+7*s(26)+3
Such that:aux(10) =< Out
it(20) =< aux(10)
aux(7) =< aux(10)+1
s(28) =< it(20)*aux(10)
s(27) =< it(20)*aux(7)
s(25) =< s(27)
s(25) =< s(28)
s(26) =< s(27)
with precondition: [Out=V,Out>=2]
* Chain [22,19]: 3
with precondition: [V=Out,V>=1]
* Chain [19]: 1
with precondition: [V=0,Out=0]
#### Cost of chains of start(V,V3,V4,V5):
* Chain [25]: 2*s(40)+7*s(41)+7*s(42)+4
Such that:s(37) =< -V3+V5+1
s(39) =< V3
s(38) =< V5+1
s(40) =< s(39)
s(41) =< s(38)
s(41) =< s(37)
s(42) =< s(38)
with precondition: [V=0]
* Chain [24]: 23*s(44)+14*s(48)+14*s(49)+7*s(54)+7*s(55)+1*s(56)+4
Such that:s(50) =< -V+V3+1
s(56) =< V3
s(51) =< V3+1
aux(11) =< V
s(44) =< aux(11)
s(54) =< s(51)
s(54) =< s(50)
s(55) =< s(51)
s(45) =< aux(11)+1
s(46) =< s(44)*aux(11)
s(47) =< s(44)*s(45)
s(48) =< s(47)
s(48) =< s(46)
s(49) =< s(47)
with precondition: [V>=1]
* Chain [23]: 1
with precondition: [V3=0,V>=0]
Closed-form bounds of start(V,V3,V4,V5):
-------------------------------------
* Chain [25] with precondition: [V=0]
- Upper bound: nat(V3)*2+4+nat(V5+1)*14
- Complexity: n
* Chain [24] with precondition: [V>=1]
- Upper bound: 51*V+4+28*V*V+nat(V3)+nat(V3+1)*14
- Complexity: n^2
* Chain [23] with precondition: [V3=0,V>=0]
- Upper bound: 1
- Complexity: constant
### Maximum cost of start(V,V3,V4,V5): nat(V3)+3+max([nat(V5+1)*14+nat(V3),28*V*V+51*V+nat(V3+1)*14])+1
Asymptotic class: n^2
* Total analysis performed in 286 ms.